﻿/*============================================
 * 类名 :MatchLaw
 * 描述 :对公式进行匹配
 *   
 * 创建时间: 2010/7/24 11:38:58
 * Blog:   http://home.cnblogs.com/xiangism
 *============================================*/
using System;
using System.Collections.Generic;

using System.Text;

namespace 命题证明
{

    /// <summary>对公式进行匹配</summary>
    class MatchLaw
    {
        ReplaceWork replace;

        /// <summary>所有可以用的推理定律</summary>
        public static List<Law> proof = LawFactory.CreateProof();
        /// <summary>所有可以用的恒等定律</summary>
        public static List<Law> equal = LawFactory.CreateEqual();

        /// <summary>和公式进行匹配,返回新得到的一系列推理节点</summary>
        public List<ProveNode> MatchProof( ReplaceWork rep, List<ProveNode> proves )
        {
            replace = rep;
            List<ProveNode> results = new List<ProveNode>();
            string after = ExpressionFactory.ConvertToAfter( replace.NewExp.Head );
            foreach ( Law l in proof )
            {
                Match( proves, results, after, l );
            }

            return results;
        }

        public List<ProveNode> MatchEqual( ReplaceWork rep, List<ProveNode> proves )
        {
            replace = rep;
            List<ProveNode> results = new List<ProveNode>();
            string after = ExpressionFactory.ConvertToAfter( replace.NewExp.Head );

            foreach ( Law l in equal )
            {
                Match( proves, results, after, l );
            }

            return results;
        }

        void Match( List<ProveNode> proves, List<ProveNode> results, string after, Law l )
        {
            List<LawFormat> formats = IsRequest( after, l );
            foreach ( LawFormat format in formats )
            {
                //string resultAfter = CallResult( after, law, l.Result.ToString( "A" ) );
                string resultAfter = CallResult( after, format.ConditionAfter, format.Result );
                replace.ReplaceBack( ref resultAfter );

                results.Add( new ProveNode( new Expression( ExpressionFactory.AfterToMiddle( resultAfter ) ), proves, l.Name ) );
            }
        }

        /// <summary>根据后序对应的后序公式和结论，得出推理结论</summary> 
        static string CallResult( string afterExp, string law, string lawResult )
        {
            string result = "";
            for ( int i = 0; i < lawResult.Length; i++ )
            {
                if ( MainChar.IsOperator( lawResult[i] ) )
                {
                    result += lawResult[i];
                }
                else
                {
                    int index = law.IndexOf( lawResult[i] );
                    result += afterExp[index];
                }
            }
            return result;
        }

        /// <summary>比较两个后序表达式是否一样，字母要对应一样 p→q 和a→b 在这里认为相等</summary> 
        static bool IsAfterEquals( string s1, string s2 )
        {
            if ( s1.Length != s2.Length )
                return false;
            for ( int i = 0; i < s1.Length - 1; i++ )
            {
                // 是字母
                if ( MainChar.IsWord( s1[i] ) )
                {
                    for ( int j = i + 1; j < s1.Length; j++ )
                    {
                        if ( s1[i] == s1[j] && s2[i] != s2[j] )
                        {
                            return false;
                        }
                    }
                }
                //是操作符
                else
                {
                    if ( s1[i] != s2[i] )
                        return false;
                }
            }
            if ( MainChar.IsOperator( s1[s1.Length - 1] ) && s1[s1.Length - 1] != s2[s1.Length - 1] )
                return false;
            return true;
        }

        /// <summary>比较一个后序形式是否符合一个公式，并且返回符合公式的所有定律形式</summary> 
        static List<LawFormat> IsRequest( string afterExp, Law law )
        {
            List<LawFormat> formats = new List<LawFormat>();
            foreach ( LawFormat after in law.AllFormats )
            {
                if ( IsAfterEquals( after.ConditionAfter, afterExp ) )
                    formats.Add( after );
            }
            return formats;
        }

    }

}
